\begin{tabbing}
$\forall$${\it es}$:ES, $R$:\{$R$:E$\rightarrow$E$\rightarrow\mathbb{P}\mid$ $\forall$$e$, ${\it e'}$:E. $R$($e$,${\it e'}$) $\Rightarrow$ (${\it e'}$ $<$ $e$)\} , $d$:($\forall$$e$, ${\it e'}$:E. Dec($R$($e$,${\it e'}$))).
\\[0ex]causal{-}predecessor(${\it es}$;es{-}r{-}pred\{i:l\}(${\it es}$;$d$;$R$))
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex](($\uparrow$can{-}apply(es{-}r{-}pred\{i:l\}(${\it es}$;$d$;$R$);$e$)) $\Leftarrow\!\Rightarrow$ ($\exists$${\it e'}$:E. $R$($e$,${\it e'}$)))
\\[0ex]\& (($\uparrow$can{-}apply(es{-}r{-}pred\{i:l\}(${\it es}$;$d$;$R$);$e$)) $\Rightarrow$ $R$($e$,do{-}apply(es{-}r{-}pred\{i:l\}(${\it es}$;$d$;$R$);$e$))))
\-
\end{tabbing}